r:. (r = 0  )  (|r| = 0  ) 

latex

Definitions	1/r, (r/s), {T}, SQType(T), True, (i = j), r * s, ff, i <z j, tt, qpositive(r), if b then t else f fi , qeq(r;s), b, |r|, , t  T, P  Q, P  Q, P & Q, P  Q, x:A. B(x), False, a  b  T , A c B, , x:A. B(x), A, P  Q, S  T
Lemmas	qeq wf2, assert of eq int, int nzero properties, q-elim, qmul wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, bool sq, qpositive wf, bool cases, assert-qeq, qabs wf, int inc rationals, rationals wf